analysis (differential/integral calculus, functional analysis, topology)
metric space, normed vector space
open ball, open subset, neighbourhood
convergence, limit of a sequence
compactness, sequential compactness
continuous metric space valued function on compact metric space is uniformly continuous
…
…
constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
A Cauchy real number is a real number that is given as the limit of a Cauchy sequence of rational numbers. One may use this idea as a definition of the general concept of real number. This is due to Georg Cantor in 1872, the same year that Richard Dedekind developed Dedekind cuts as a definition of the same concept.
If we simply want a construction of the real line for the purposes of classical mathematics, then we can use Cantor's original version. If we wish to use weak foundations or internalise the Cauchy real line, then there are subtler alternatives.
Putting Cantor's definition in modern terminology, is the quotient set of the set of Cauchy sequences of rational numbers, with two sequences considered equivalent if their difference converges to zero. Although the notion of Cauchy sequence (and convergence, for that matter) is best known in the context of metric spaces (which cannot be defined in general without having, at least implicitly, constructed already), it is easy to state the definitions in elementary terms. (We can also view these as Cauchy sequences in a Booij premetric space.) If there is any tricky point, it is that the requirements made for all need be made only for rational . (We could also treat as a uniform space or even a Cauchy space, although again to write down the definitions of those structures still requires one to handle the s.)
To be explicit: A Cauchy real number is an infinite sequence of rational numbers such that, for every positive rational number , there exists a natural number such that
holds whenever . Two Cauchy real numbers are considered equal if, for every positive rational number , there exists a natural number such that
holds whenever . It is easy to prove that this is an equivalence relation on the set of Cauchy sequences, so the set of real numbers is a quotient set.
This definition comes in two steps: one to identify the Cauchy sequences from among the infinite sequences, another to identify equivalent sequences. Actually, we can do this in one step by placing a partial equivalence relation on the set of all infinite sequences of rational numbers. Two sequences are considered equivalent if, for every positive rational number , there exists a natural number such that
holds whenever . It is immediate that a sequence is Cauchy if and only if it equivalent to itself, and it is easy to prove that two Cauchy sequences are equivalent if and only if they are equal as real numbers using the definition above. Thus, we can construct immediately as a subquotient of the function set .
In weak foundations, we sometimes want to be a little more strict about how a sequence is Cauchy and how the difference of two such sequences converges to zero. We do this by requiring explicit moduli of convergence. These moduli can always be constructed using (for example) either countable choice or the principle of excluded middle, but the requirement makes a difference in (for example) a localic topos over any non-discrete space.
(Since the term ‘Cauchy real number’ is used ambiguously in the constructive literature, we can identify Cantor's classical definition above as a Cantor real number or a classical Cauchy real number.)
In general, a modulus of convergence may be any function from the positive rational numbers to the natural numbers such that, for every natural number , there is a positive rational number such that .
A modulated Cauchy real number or regular real number is an infinite sequence of rational numbers such that there exists a modulus such that
holds whenever . Two modulated Cauchy real numbers are considered equal if there exists a modulus such that
holds whenever . Again we can combine these conditions into a single partial equivalence relation: that there exists a modulus such that
holds whenever .
Some variations are often met. A modulus may be extended to all rational numbers, although the conditions above can only be required for positive . Alternatively, it is enough to define (and require the conditions) for of specific form; common choices are and for a natural number, which work well with and , respectively. (The important criterion is to use a detachable set of positive rational numbers of which zero is a limit point; then can be extended from this set to all positive rational numbers by rounding down.)
It is also possible to fix a specific modulus ahead of time. Then we need to treat each index separately, in this way: An -regular Cauchy real number is an infinite sequence of rational numbers such that
holds whenever and . Two -regular Cauchy real numbers are considered equal if
holds whenever . Once more, we can combine these conditions into a single partial equivalence relation: that
holds whenever and .
The modulated Cauchy real numbers could also be constructed through Cauchy approximations rather than sequences of rational numbers with a modulus of convergence. Let be the rational numbers and let
be the positive rational numbers.
Let us define a modulated Cauchy algebra to be a set with a function , where is the set of Cauchy approximations in and is the set of functions with domain and codomain , such that
A modulated Cauchy algebra homomorphism is a function between modulated Cauchy algebras and such that
The category of modulated Cauchy algebras is the category whose objects are modulated Cauchy algebras and whose morphisms are modulated Cauchy algebra homomorphisms. The set of modulated Cauchy real numbers, denoted , is defined as the initial object in the category of modulated Cauchy algebras.
The modulated Cauchy real numbers are a quotient inductive type inductively generated by the following:
a function , where is the type of Cauchy approximations in .
a dependent family of terms
a family of dependent terms
This is the approach of Booij20
While requiring a modulus of convergence, even fixing the modulus of convergence, may be more restrictive, it is also possible to use a potentially more lax definition.
One way is to use multivalued functions from the natural numbers. A multivalued Cauchy real number is an entire relation between natural numbers and rational numbers such that, for every positive rational number , there exists a natural number such that, whenever ,
holds for some such that and hold. Two multivalued Cauchy real numbers are considered equal if, for every positive rational number , there exists a natural number such that, whenever ,
holds for some such that and hold. The partial equivalence relation subsuming both conditions is that, for every positive rational number , there exists a natural number such that, whenever ,
holds for some such that and .
Another way is to use nets (also called ‘generalised sequences’). A generalised Cauchy real number is a net (where is any directed set of indices) of rational numbers such that, for every positive rational number , there exists an index in such that
holds whenever in . Two generalised Cauchy real numbers are considered equal if, for every positive rational number , there exists an index for and an index for such that
holds whenever and . Actually, this is already a partial equivalence relation on all nets which subsumes both conditions.
Requiring a modulus of convergence would make no difference for either of these, since we would expect such a modulus to also to be either multivalued or given by a net, and these are easy to construct explicitly (even in constructive mathematics).
(Since the term ‘Cauchy real number’ logically applies just as well to these generalisations, we may speak of sequential real numbers for the classical or modulated version.)
Classically, all of these definitions are equivalent. In fact, to prove their equivalence, we need only the following equivalent principles (cf. Booij 2020):
Every Dedekind real number is a modulated Cauchy real number
For every Dedekind real number there exists a signed-digit radix representation of the real number
For every Dedekind real number there exists a locator
For every Dedekind real number there exists Dedekind cut structure
For every Dedekind real number there exists a Cauchy sequence of rational numbers whose limit is the real number.
If we don't accept any of the above, then we still have these results:
(constructive).
Given any modulus of convergence , every -regular Cauchy real number is a modulated Cauchy real number. Furthermore, any two -regular real numbers are equal as -regular real numbers if and only if they are equal as modulated Cauchy real numbers. Conversely, every modulated Cauchy real number is equal (as a modulated Cauchy real number) to some -regular Cauchy real number.
Every modulated Cauchy real number is a classical Cauchy real number, and any two equal modulated Cauchy real numbers are equal as classical Cauchy real numbers.
Every classical Cauchy real number is a multivalued Cauchy real number, and any two equal classical Cauchy real numbers are equal as multivalued Cauchy real numbers.
Every multivalued Cauchy real number becomes a generalised Cauchy real number whose index set comes equipped with a surjection to the natural numbers. Furthermore, any two multivalued Cauchy real numbers are equal as multivalued Cauchy real numbers if and only if they are equal as generalised Cauchy real numbers. Conversely, any generalised Cauchy real number is equal (as a generalised Cauchy real number) to some multivalued Cauchy real number.
Every generalised Cauchy real number becomes a Dedekind real number in the usual way, defining lower and upper sets in terms of the order relation on generalised Cauchy real numbers. Furthermore, any two generalised Cauchy real numbers are equal as generalised Cauchy real numbers if and only if they are equal as Dedekind cuts. Conversely, any Dedekind cut is equal (as a Dedekind cut) to some generalised Cauchy real number.
Hence even in constructive mathematics, there are only three notions that we need consider: modulated Cauchy real numbers, classical Cauchy real numbers, and Dedekind real numbers; and there is a function from each of these to the next.
Just to be explicit, here are the missing converses:
Every classical Cauchy real number is modulated, and any two equal Cauchy real numbers are equal as modulated Cauchy real numbers.
Every multivalued Cauchy real number is equal (as a multivalued Cauchy real number) to some classical Cauchy real number, and two classical Cauchy real numbers are equal if they are equal as multivalued Cauchy real numbers.
Most practitioners of both constructive mathematics and topos theory want to use the Dedekind real numbers. Without excluded middle or countable choice, the classical Cauchy real numbers are not very well behaved. The modulated Cauchy real numbers, however, do have their good points; for example, the fundamental theorem of algebra is simplest for them. They also make sense in predicative mathematics with function sets, whereas multivalued Cauchy reals require fullness and the Dedekind reals require powersets for their definitions.
On the other hand, even the (modulated) Cauchy real numbers are not necessarily Cauchy complete, i.e. a Cauchy sequence (even a modulated one) of Cauchy real numbers need not converge to another Cauchy real number (though it always does converge to a Dedekind real number, since the Dedekind real numbers are always Cauchy complete). The problem is that without enough countable choice, we cannot lift a (modulated) Cauchy sequence of (modulated Cauchy) real numbers to a Cauchy sequence of Cauchy sequences in order to “diagonalize” it; a countermodel is constructed by Lubarsky.
For non-modulated Cauchy sequences and reals, there are additional problems even if we assume representatives are already chosen. A modulated Cauchy sequence of modulated Cauchy sequences does converge to a modulated Cauchy sequence. Moreover, a modulated Cauchy sequence of classical Cauchy sequences, and a classical Cauchy sequence of modulated Cauchy sequences, both necessarily converge to a classical Cauchy sequence. But the results need not be modulated, and a classical Cauchy sequence of classical Cauchy sequences need not converge to a classical Cauchy sequence. In fact, Lubarsky shows that:
The generic classical Cauchy sequence, in the classifying topos of classical Cauchy sequences, is not modulated. Thus, we cannot prove that every classical Cauchy sequence is modulated. Hence, we cannot prove that a classical Cauchy sequence of modulated Cauchy sequences has a modulated limit (since a classical Cauchy sequence of rationals can be regarded as a classical Cauchy sequence of (constant) modulated Cauchy sequences).
The generic classical Cauchy sequence of classical Cauchy sequences, in the classifying topos of such, does not converge to a classical Cauchy sequence.
The generic modulated Cauchy sequence of classical Cauchy sequences, in the classifying topos of such, does not converge to a modulated Cauchy sequence.
(Actually, Lubarsky writes using Heyting-valued sets? on topological spaces rather than classifying toposes of propositional geometric theories, but it seems almost certain to me that his results can be rephrased as the above.)
Let be an Archimedean ordered field. Every element of satisfies the axioms of a Dedekind cut with respect to the strict order relation of , and is thus a real number.
The Dedekind real numbers are the terminal Archimedean ordered field, i.e. for any other Archimedean ordered field , there exists a unique strictly monotonic field homomorphism . Since every ring homomorphism between fields is an injection, the Dedekind real numbers being the terminal Archimedean ordered field implies that every other Archimedean ordered field is a subfield of via the unique ring homomorphism :
In this sense, the Dedekind real numbers is the collection of all real numbers.
An element is a Cauchy real number if there exists a locator of . The Cauchy real numbers are the set of Dedekind real numbers where there exist a locator
Alternatively, if one doesn’t have the Dedekind real numbers, then one can still characterize the Cauchy real numbers by its universal property. The Cauchy real numbers is the terminal Archimedean ordered field where for every element there exists a locator of : i.e. for any other Archimedean ordered field where for every element there exists a locator of , there exists a unique strictly monotonic field homomorphism .
Since every ring homomorphism between fields is an injection, the Cauchy real numbers being the terminal Archimedean ordered field where for every element there exists a locator of implies that every other such Archimedean ordered field is a subfield of via the unique ring homomorphism :
In this sense, the Cauchy real numbers is the collection of all real numbers for which there exist a locator.
Either way, this definition makes sense in any Heyting category with exponential objects and a natural numbers object, even when the Heyting category is not a pretopos and the Cauchy real numbers cannot be constructed as a quotient set. In classical mathematics, one can prove that the Dedekind real numbers is a discrete field, which implies that the Cauchy real numbers and the Dedekind real numbers coincide.
In dependent type theory, the property that there exists a locator of is rendered as the bracket type of the type of locators of .
In addition, the Cauchy real numbers is not to be confused with the set of (real number, locator) pairs
The latter set is equivalent to the set of Cauchy sequences of rational numbers. Rather, the Cauchy real numbers are the image of the projection function from to which takes a (real number, locator) pair to its constituent real number.
The algebraic closure of the modulated Cauchy real numbers is the modulated Cauchy complex numbers; i.e. the fundamental theorem of algebra is true for the modulated Cauchy real numbers.
Although the notion of metric space doesn't make sense until we know what real numbers are, once we have these, we can recognise that the rational numbers form a metric space and the real numbers were constructed from them in a way that makes reference only to the metric-space structure of . Thus, this procedure may be generalised to any metric space to produce its completion.
We can also interpret as a uniform space or even as a Cauchy space and define analogous notions of completion for these. However, these require us (in general) to use generalised Cauchy sequences, that is Cauchy nets, even in classical mathematics. (Of course, without excluded middle or countable choice, we should use nets even for metric spaces.)
Suppose that we wish to approximate a real number by common fractions with arbitrarily large denominators. That is, given any natural number , we wish to find integers such that is within of . Then the sequence of values is an -regular Cauchy real with as modulus of convergence. (You can extend to every positive rational number by , but that is not important.) Conversely, given an -regular Cauchy real for this modulus , we can round each (for ) to the nearest rational number with denominator (which can be done using only rational arithmetic) to produce an equal -regular Cauchy real.
We might instead want to approximate by arbitrarily long decimal fractions. That is, given any natural number , we wish to find integers such that is within of . Now the sequence of values is an -regular Cauchy real with as modulus of convergence. Conversely, we can round off the values of any -regular Cauchy real as before. Of course, there is nothing special about the base here; for theoretical purposes, base is popular.
Thus, to define a real number to be an -regular Cauchy real (for any of these choices of ) is to make into a definition our intuition that we can round real numbers in this way.
Note we may be rounding up or down, regardless of which is nearer. For example, in approximating by decimal fractions, we might get ( or , but we might also get . To choose to always round down, towards zero, or towards the nearer approximant (with a rule for ) requires an application of excluded middle (or at least the lesser limited principle of omniscience).
Even for Dedekind reals in neutral constructive mathematics, we can always approximate a real number in this way up to any given . Choice is needed only to make infinitely many approximations at once. Trying to avoid this can motivate multivalued Cauchy real numbers.
See also the references at real number and constructive analysis.
Original articles:
Dicussion in constructive analysis:
Errett Bishop: Foundations of Constructive Analysis, McGraw-Hill (1967)
Errett Bishop, Douglas Bridges: Constructive Analysis, Grundlehren der mathematischen Wissenschaften 279, Springer (1985) [doi:10.1007/978-3-642-61667-9]
Fred Richman, Douglas Bridges, Peter Schuster, A weak countable choice principle. Proceedings of the American Mathematical Society 128(9):2749-2752, March 2000. [doi:10.1090/S0002-9939-00-05327-2]
The proof that Cauchy sequences (with a modulus of convergence) as such (i.e. not passing to their equivalence classes) are sequentially Cauchy complete:
See also
On why the (modulated) Cauchy real numbers, hence after passage to equivalence classes of Cauchy sequences, are not sequentially Cauchy complete (without the axiom of countable choice):
See also
A constructive algebraic proof of the fundamental theorem of algebra for the modulated Cauchy real numbers without countable choice:
Implementation of Bishop-style Cauchy real numbers in Agda:
Martin Lundfall, Formalizing real numbers in Agda (2015) [pdf, pdf, github]
Zachary Murray, Constructive Analysis in the Agda Proof Assistant [arXiv:2205.08354, github]
review:
A novel construction principle of the type of real numbers, as a higher inductive-inductive type in univalent homotopy type theory, not reliant on representatives by sequences of rational numbers, and with provable Cauchy completeness even without extra axiom of countable choice is laid out (cf. HoTT book real numbers) in
but has not yet been implemented in any proof assistant,
Exposition and review:
Andrej Bauer, The real numbers in homotopy type theory, talk at Computability and Complexity in Analysis, Faro (2016) [pdf, pdf]
Auke Booij, Analysis in Univalent Type Theory (2020) [etheses:10411, pdf, pdf]
Last revised on July 10, 2024 at 00:08:18. See the history of this page for a list of all contributions to it.